|
In mathematical logic, an uninterpreted function〔Bryant, Lahiri, Seshia (2002) "Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions". ''Computer Aided Verification'' 2404/2002, 106–122.〕 or function symbol is one that has no other property than its name and arity. Function symbols are used, together with constants and variables, to form terms. The theory of uninterpreted functions is also sometimes called the free theory, because it is freely generated, and thus a free object, or the empty theory, being the theory having an empty set of sentences (in analogy to an initial algebra). Theories with a non-empty set of equations are known as equational theories. The satisfiability problem for free theories is solved by syntactic unification; algorithms for the latter are used by interpreters for various computer languages, such as Prolog. Syntactic unification is also used in algorithms for the satisfiability problem for certain other equational theories, see E-Unification and Narrowing. ==Example== An array can be specified by the following equational axiom:〔Here, ''select''(''a'',''i'') informally designates the value of the ''i''th element of ''a'', written e.g. in C as a(), while ''store''(''a'',''i'',''v'') informally designates the array resulting from writing the value ''v'' to the ''i''th element of ''a'', written in C as a()=v.The axiom then informally means that the value obtained by the statements a()=v;return a(); equals v if i=j, and a(), else.〕: ''select''(''store''(''a'',''i'',''v''),''j'') = (if ''i'' = ''j'' then ''v'' else ''select''(''a'',''j'')) This axiom can be used to deduce〔This deduction corresponds to the computation of the value obtained by a()=-1;a()=-2;return a();〕: ''select''(''store''(''store''(''a'',1,−1),2,−2),1) :: = ''select''(''store''(''a'',1,−1),1) :: = −1 Note that this reasoning did ''not'' use any 'definition' or interpretation for the functions ''select'' and ''store''. All that is known is the axiom. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Uninterpreted function」の詳細全文を読む スポンサード リンク
|